2017年5月12日上午，全球人终于明白互联网上不全是音乐和鲜花。一个名为“永恒之蓝(WannaCry)”的勒索病毒袭击了全球上百个国家和地区使用微软Windows操作系统的电脑，让世人感叹，原来网上的江湖波谲云诡、危机四伏。

怎样打造攻不破、摧不垮、百毒不侵的电脑？怎样才能还网民太平？科学家们为了维持网络的稳定，真是操碎了心。

2015年夏天，一群黑客企图控制一架名为“小鸟”(LITTLE BIRD H-6U)的军用无人直升机。“小鸟”是位于美国亚利桑那州的波音工厂为美军特种作战任务研制的专用飞机。当时，黑客们开始入侵时，即“攻占”了无人直升机上电脑系统的一部分。他们的计划是：只需入侵“小鸟”的飞行控制电脑，这架无人直升机就是他们的了。起初，黑客团队可以像入侵家庭Wi-Fi一样轻松地接管直升机，易如囊中探物。但在随后的几个月里，美国国防部高级研究计划署(DARPA)的工程师们开发了一种“百毒不侵”的软件系统，并实施了一种新型的安全机制，使得“小鸟”计算机系统的关键部分根本无法入侵，其代码的正确性和可靠性能像数学定理一样被证明。因此，尽管无人直升机的计算机网络完全开放，黑客团队也一直无法掌握“小鸟”的控制系统。黑客们经过连续六周的攻击都不能越雷池一步，以彻底失败告终。

压制黑客是一种称为形式化方法¹的软件编程技术。过去对传统计算机代码的评估主要是检查它是否能在各种情况下正常工作，而软件形式化验证如同数学定理证明：程序中每个语句的前后都遵循严格的逻辑关系，整个程序测试的确定性就像数学家证明定理一样。

大多数传统计算机的程序是如何工作的呢？我们可以设想为无人驾驶汽车编写一个计算机程序。在操作层面上，可以定义汽车在行驶过程中的各种必要的操作行为，例如左转、右转、制动或加速。而程序是按照适当顺序排列的基本操作的汇编，以确保汽车到达杂货店而不是机场。

长期以来，对此类程序的评估和验收都是进行简单的测试，即把各种起始位置和目标位置输入程序，检查无人驾驶汽车在程序控制下是否正确到达预定目标。在大多数情况下，这种测试方法可以满足我们的要求。但是，这种方法不能保证软件完全正常地工作，因为各种输入和输出的组合无穷无尽，现实环境中总会有罕见的情况发生，总会有不能预测到的“角落”，从而导致程序出错。在程序的运行中，这些错误和故障当然不允许出现，但更大的危害是可能引起计算机内存缓冲区溢出，为黑客攻击系统提供跳板，软件中的任何一个缺陷都可能是系统安全的漏洞。

再举一个例子，编写对一串数字进行排序的程序。程序员对排序程序的定义可能会写成这样：

对于列表中的每个元素j，确保元素j≤元素j+1

然而，这种定义——确保列表中的每个元素小于或等于其后面的元素——忽略了一个隐含的需求：输出总是输入的一种置换。也就是说，对于输入列表[9, 2, 5]，期望程序输出结果为[2, 5, 9]，以满足排序定义。但是列表[2, 5, 7]也同样满足定义，它也是一个排序列表，但是它不是程序员希望得到的排序列表。严格地说，除了满足排序定义，还必须确保输出与输入的元素集合完全一致。

将一个程序应该做些什么的想法转化为一个形式化的规约，同时又要排除可能产生的各种不正确的解释，这常常是十分困难的。上述例子只是一个简单的排序程序。如果是比排序更抽象的程序，比如密码保护，在数学上又是什么意思呢？它可能涉及对密码保护进行数学描述，或者对加密算法的安全性做出定义。

2017年5月12日上午，全球人终于明白互联网上不全是音乐和鲜花。一个名为“永恒之蓝(WannaCry)”的勒索病毒袭击了全球上百个国家和地区使用微软Windows操作系统的电脑，让世人感叹，原来网上的江湖波谲云诡、危机四伏。

怎样打造攻不破、摧不垮、百毒不侵的电脑？怎样才能还网民太平？科学家们为了维持网络的稳定，真是操碎了心。

2015年夏天，一群黑客企图控制一架名为“小鸟”(LITTLE BIRD H-6U)的军用无人直升机。“小鸟”是位于美国亚利桑那州的波音工厂为美军特种作战任务研制的专用飞机。当时，黑客们开始入侵时，即“攻占”了无人直升机上电脑系统的一部分。他们的计划是：只需入侵“小鸟”的飞行控制电脑，这架无人直升机就是他们的了。起初，黑客团队可以像入侵家庭Wi-Fi一样轻松地接管直升机，易如囊中探物。但在随后的几个月里，美国国防部高级研究计划署(DARPA)的工程师们开发了一种“百毒不侵”的软件系统，并实施了一种新型的安全机制，使得“小鸟”计算机系统的关键部分根本无法入侵，其代码的正确性和可靠性能像数学定理一样被证明。因此，尽管无人直升机的计算机网络完全开放，黑客团队也一直无法掌握“小鸟”的控制系统。黑客们经过连续六周的攻击都不能越雷池一步，以彻底失败告终。

压制黑客是一种称为形式化方法¹的软件编程技术。过去对传统计算机代码的评估主要是检查它是否能在各种情况下正常工作，而软件形式化验证如同数学定理证明：程序中每个语句的前后都遵循严格的逻辑关系，整个程序测试的确定性就像数学家证明定理一样。

大多数传统计算机的程序是如何工作的呢？我们可以设想为无人驾驶汽车编写一个计算机程序。在操作层面上，可以定义汽车在行驶过程中的各种必要的操作行为，例如左转、右转、制动或加速。而程序是按照适当顺序排列的基本操作的汇编，以确保汽车到达杂货店而不是机场。

长期以来，对此类程序的评估和验收都是进行简单的测试，即把各种起始位置和目标位置输入程序，检查无人驾驶汽车在程序控制下是否正确到达预定目标。在大多数情况下，这种测试方法可以满足我们的要求。但是，这种方法不能保证软件完全正常地工作，因为各种输入和输出的组合无穷无尽，现实环境中总会有罕见的情况发生，总会有不能预测到的“角落”，从而导致程序出错。在程序的运行中，这些错误和故障当然不允许出现，但更大的危害是可能引起计算机内存缓冲区溢出，为黑客攻击系统提供跳板，软件中的任何一个缺陷都可能是系统安全的漏洞。

再举一个例子，编写对一串数字进行排序的程序。程序员对排序程序的定义可能会写成这样：

对于列表中的每个元素j，确保元素j≤元素j+1

然而，这种定义——确保列表中的每个元素小于或等于其后面的元素——忽略了一个隐含的需求：输出总是输入的一种置换。也就是说，对于输入列表[9, 2, 5]，期望程序输出结果为[2, 5, 9]，以满足排序定义。但是列表[2, 5, 7]也同样满足定义，它也是一个排序列表，但是它不是程序员希望得到的排序列表。严格地说，除了满足排序定义，还必须确保输出与输入的元素集合完全一致。

将一个程序应该做些什么的想法转化为一个形式化的规约，同时又要排除可能产生的各种不正确的解释，这常常是十分困难的。上述例子只是一个简单的排序程序。如果是比排序更抽象的程序，比如密码保护，在数学上又是什么意思呢？它可能涉及对密码保护进行数学描述，或者对加密算法的安全性做出定义。

使用形式逻辑规则来指导程序设计起源于20世纪70年代。艾兹格·迪科斯彻(Edsger Dijkstra)首先提出了创建无错代码的想法。他在1976年完成的著作《编程的修炼》(A Discipline of Programming)为程序验证打下了基础，他也因此获得了图灵奖。

70年代末，我在上海交通大学攻读硕士，我的两位同门师兄的选题就是“程序设计自动化验证”，可见当时我国高校对世界科技动向还是很敏感的。当时硕士生课题大多很“高大上”，但是严重脱离实际，且缺少对课题项目的长期规划和投入，估计也很难有实质性的收获。

将正确性证明纳入计算机程序开发一直没有得到广泛的应用，计算机科学的发展毕竟不能单纯依靠愿望。一直以来，使用形式逻辑规则来指定程序的功能不是不可能，但却是不现实的。包含形式化验证信息的程序长度可能是传统程序的5倍。这种编程的额外负担可以通过专用的编程语言和辅助软件工具适当减轻，但是这种辅助软件工具在20世纪七八十年代并不存在。即使辅助软件工具有所改进，推广程序验证的更大障碍是：没有人确定是否有必要。虽然一些专家一再强调编码中的小错误会导致灾难性的后果，但是人们看到的是，大多数情况下计算机程序工作正常。当然，偶尔会丢失数据或蓝屏死机，可是让文秘重新输入数据或者偶尔重新启动计算机也没有什么大不了的。

但是，互联网改变了一切。如同航空旅行的普及导致传染病的飞速传播一样，当计算机互相连接在一起，一台计算机的编码错误就可能会被黑客利用，导致成千上万台计算机被非法入侵控制，甚至使网络局部瘫痪。就像今年5月12日勒索病毒爆发那样，全球网民都尝到了苦头。

当研究人员开始了解互联网对计算机安全的威胁时，程序验证技术终于有了用武之地。首先，研究人员在基于形式化方法的编程技术上取得了巨大进步：改进了支持形式化方法的Coq和Isabelle等验证辅助程序；开发了一种称为dependent-type theories的新的逻辑系统，为计算机对代码的推理提供了全新的框架；改进了所谓的“操作语义”——本质上是一种具有确切词汇的语言，可以更明确地表达程序究竟应该做什么。

美国高保证网络军事系统(HACMS)项目，显示了如何通过计算机系统分区隔离，以保证总体的安全。该项目的第一个目标是创造一个无法入侵的娱乐级四轴飞行器。运行该飞行器的商品化软件是整体单一化的，这意味着，如果攻击者突破一个点，就可以控制整个软件。于是在之后的两年内，HACMS团队将四轴飞行器任务控制计算机中的代码进行了分区隔离。同时，他们还重新制定了软件架构，使用了一种可以帮助程序员证明其代码正确无误的工具，这种工具被HACMS项目经理凯瑟琳·费舍尔称为“高保证构建块”。其中一个经过验证的构建块可以保证在某个分区内具有访问权限的操作者无法升级越界进入其他分区。

高保证网络军事系统(HACMS)项目主管凯瑟琳·费舍尔

根据四轴飞行器取得的经验，研究人员在“小鸟”军用无人直升机上也安装了这个分区隔离软件。在测试中，他们允许黑客团队进入无人直升机的某一分区，例如，摄相机控制分区，但并不是核心功能分区。在无情的数学公式面前，黑客被死死地卡在一个分区中。“他们以机器检查的方式证明，黑客不能脱离分区，这毫不奇怪，他们就是不能。”凯瑟琳·费舍尔说：“这与定理是一致的，试验也证明了这一点。”

20世纪中期，中国绝密军工厂的管理方式与计算机系统的分区隔离技术的基本原理在一定程度上类似。这类军工厂不仅门卫森严，而且内部分成密级不同的独立车间，不同车间的人员不得互相来往。每个产品必须由多个车间加工生产。一个间谍（黑客）进入工厂并混进某个车间已经非常不易，即使他下足工夫，取得车间主任的信任而获得某种特权，但他也只能在一个车间内活动，他对整个产品的认识和控制依然十分有限，因为任何试图跨越车间界限的行为会被严格地限制，而且其真实身份会立刻受到特别调查。

近年来，计算机硬件性能的飞速进步也为计算机系统的分区隔离技术提供了物质基础，强大的中央处理器能力和海量的内存空间完全可以支持系统的分区运行管理。

在“小鸟”无人直升机上经过测试后，DARPA正努力将HACMS项目的工具和技术应用于其他军事技术领域，如卫星和无人自动驾驶车队。

为了捍卫互联网的安全，形式化方法的研究人员正在推动更加雄心勃勃的计划。DeepSpec合作项目力图将过去十年中已经成功通过形式化验证的许多小型模块进行组合，以构建一个完全经过形式化验证的端到端系统，如Web服务器。

在微软的研究部门，软件工程师正在进行两项雄心勃勃的形式化验证项目。第一个名为“珠穆朗玛峰”，即创建一个经过形式化验证的HTTPS²版本，以有效地保护被称为“互联网的阿喀琉斯之踵”的网络浏览器；第二个是为复杂的网络物理系统（如无人机）制定形式化验证规范。后者难度更大。无人机涉及机器学习，以及在连续的环境数据流中进行概率判定，如何对不确定性进行推理并制定形式化规范是极大的挑战。在过去的十年中，软件工程的形式化方法研究已经有了长足的进步，从事该项研究的科学家们对未来持谨慎乐观的态度。 ■

脚注：

¹ 形式化方法(formal method)是基于严密的、数学上的形式机制的计算机系统研究方法，该知识体系中有6个主要领域，分别为基础(foundations)、形式化规格(formal specification paradigms)、正确性验证及演算(correctness verification and calculation)、形式化语义(formal semantics)、可执行规范支持(support for executable specification)、其他(other topics)。

² 为了数据传输的安全，HTTPS在HTTP的基础上加入了安全套接字层(Secure Sockets Layer, SSL)协议，SSL依靠证书来验证服务器的身份，并为浏览器和服务器之间的通信加密。